Nuprl Lemma : no_repeats-pairs-fpf
11,40
postcript
pdf
A
,
B
:Type,
eq1
:EqDecider(
A
),
eq2
:EqDecider(
B
),
L
:((
:
A
B
) List).
no_repeats(
A
;fpf-domain(fpf(
L
)))
latex
Definitions
EqDecider(
T
)
,
no_repeats(
T
;
l
)
,
t
T
,
P
&
Q
,
x
:
A
.
B
(
x
)
Lemmas
deq
wf
,
pairs-fpf
property
origin
A, B:Type, eq1:EqDecider(A), eq2:EqDecider(B), L:((:A 
B) List).
A, B:Type, eq1:EqDecider(A), eq2:EqDecider(B), L:((:A B) List).
Tx:A. B(x)